Step of Proof: order_split 12,41
Inference at * 
Iof proof for Lemma order split:


  T:Type, R:(TT).
  Order(T;x,y.R(x,y))
   (x, y:T. Dec(x = y))
   (a, b:T. R(a,b)  (strict_part(x,y.R(x,y);a;b)  (a = b))) 
latex
 by ((((Unfold `strict_part` 0) 
CollapseTHEN (AGenRepD ["compound";"basic"]))) 
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 
latex

C1: 

C1: 1. T : Type
C1: 2. R : TT
C1: 3. a:T. R(a,a)
C1: 4. a, b, c:T. R(a,b)  R(b,c)  R(a,c)
C1: 5. x, y:T. R(x,y)  R(y,x)  (x = y)
C1: 6. x, y:T. Dec(x = y)
C1: 7. a : T
C1: 8. b : T
C1: 9. R(a,b)
C1:   (R(a,b) & (R(b,a)))  (a = b)
C2: 

C2: 1. T : Type
C2: 2. R : TT
C2: 3. a:T. R(a,a)
C2: 4. a, b, c:T. R(a,b)  R(b,c)  R(a,c)
C2: 5. x, y:T. R(x,y)  R(y,x)  (x = y)
C2: 6. x, y:T. Dec(x = y)
C2: 7. a : T
C2: 8. b : T
C2: 9. (R(a,b) & (R(b,a)))  (a = b)
C2:   R(a,b)
C.

Definitionsx,y. t(x;y), t  T, P  Q, P & Q, strict_part(x,y.R(x;y);a;b), P  Q, P  Q, x(s1,s2), P  Q, , x:A. B(x), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Order(T;x,y.R(x;y))
Lemmasorder wf, decidable wf, not wf

origin